Issue216.agda:8,11-26
Set (lsuc i) != Set i
when checking that the expression (R : Set i) → R has type Set i
